| Definitions | s = t, t  T, x:A  B(x),  x:A. B(x), Id, Type, type List, Atom$n,  b,  A, Void, P   Q, False, chain sys ind csupdate compseq tag def, csinput?(x), csupdate(from;cmds), True, csupdate?(x), {T}, P  Q, left + right, Dec(P), x:A  B(x),  x:A. B(x), b | a, a ~ b, a  b, a <p b, a < b, A c B, f(a), x f y, xL. P(x), (xL.P(x)), r s, r < s, q-rel(r;x), Outcome, (x l), l_disjoint(T;l1;l2), (e <loc e'), e loc e' , (e < e'), e c e', e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), chain sys ind csinput compseq tag def, csinput(cmd), strong-subtype(A;B), #$n,  ,  , chain_sys(Cmd),  x.A(x),  , a:A fp B(a),  x. t(x) |